package substitution;

import java.util.HashMap;
import java.util.Iterator;
import java.util.Map;

import terms.Call;
import terms.Function;
import terms.AbstractTerm;
import terms.Variable;
import tests.Constants;

/**
 * Unification algorithm coded through HashMap instead of equations Mar 31, 2012
 * Ecole des Mines de Nantes Major in Information and Communications Systems
 * Engineering.
 * @author Pierre Reliquet, Simon Devineau
 */
public class HashUnifier {
    /**
     * Return true if the object is a Variable.
     * @param anObject
     *            the term to test
     * @return true if anObject is a Variable
     */
    public static boolean isVariable(final Object anObject) {
        return anObject instanceof Variable;
    }

    /**
     * The hashmap used to store the equations.
     */
    private final transient Map<AbstractTerm, AbstractTerm> map = new HashMap<AbstractTerm, AbstractTerm>();

    /**
     * Try to add the HashMap the pair.
     * @param var
     *            the key which is the left side of the equation
     * @param term
     *            the value which is the right side of the equation
     */
    public void addToHashMap(final Variable var, final AbstractTerm term) {
        if (this.map.containsKey(var)) {
            this.unify(this.map.get(var), term);
        }
        else {
            this.map.put(var, term);
        }
    }

    /**
     * @return the map
     */
    public Map<AbstractTerm, AbstractTerm> getMap() {
        return map;
    }

    /**
     * Reduce the equations grouped in the HashMap.
     */
    public void reduce() {
        final Iterator<AbstractTerm> keyIterator = this.map.keySet().iterator();
        while (keyIterator.hasNext()) {
            final AbstractTerm key = keyIterator.next();
            final AbstractTerm right = this.map.get(key);
            for (AbstractTerm aTerm : right.getRest()) {
                if (this.map.containsKey(aTerm)) {
                    this.map.put(key,
                            substitute(right, aTerm, this.map.get(aTerm)));
                }
            }
        }
    }

    /**
     * Substitute a term by another one.
     * @param global
     *            the global term in which the term to replace is contained
     * @param toSustitute
     *            the term to replace.
     * @param replacement
     *            the value to put.
     * @return the new term.
     */
    public static AbstractTerm substitute(final AbstractTerm global,
            final AbstractTerm toSustitute, final AbstractTerm replacement) {
        AbstractTerm result = global;
        if (global instanceof Call) {
            final Call toReturn = new Call(new Function(global.getName(),
                    global.getLength() - 1));
            for (AbstractTerm term : global.getRest()) {
                if (term.equals(toSustitute)) {
                    toReturn.addTerm(replacement);
                }
                else {
                    toReturn.addTerm(term);
                }
            }
            // return toReturn;
            result = toReturn;
        }
        return result;
    }

    /**
     * @return a String representation of the equations;
     */
    @Override
    public String toString() {
        final StringBuffer buffer = new StringBuffer(50);
        final Iterator<AbstractTerm> currentKey = this.map.keySet().iterator();
        buffer.append("Equations : \n\t{");
        while (currentKey.hasNext()) {
            final AbstractTerm key = currentKey.next();
            final AbstractTerm right = this.map.get(key);
            buffer.append(key + Constants.EQUAL + right);
            if (currentKey.hasNext()) {
                buffer.append(" ; ");
            }
        }
        buffer.append('}');
        return buffer.toString();
    }

    /**
     * Unifies two terms.
     * @param first
     *            term.
     * @param second
     *            term
     */
    public void unify(final AbstractTerm first, final AbstractTerm second) {
        System.out.println("Réduction de " + first + Constants.EQUAL + second);
        if (isVariable(first) && isVariable(second)) {
            System.out.println("Résultat = { }");
        }
        else if (isVariable(first)) {
            System.out.println("Résultat {" + first + Constants.EQUAL + second
                    + "}");
            this.addToHashMap((Variable) first, second);
        }
        else if (isVariable(second)) {
            System.out.println("Résultat {" + second + Constants.EQUAL + first
                    + "}");
            this.addToHashMap((Variable) second, first);
        }
        else {
            if (!first.getName().equals(second.getName())
                    || first.getLength() != second.getLength()) {
                System.err.println("Unification failed : " + first.getName()
                        + "!=" + second.getName());
                return;
            }
            final Iterator<AbstractTerm> currentFirst = first.getRest()
                    .iterator();
            final Iterator<AbstractTerm> currentSecond = second.getRest()
                    .iterator();
            while (currentFirst.hasNext() && currentSecond.hasNext()) {
                this.unify(currentFirst.next(), currentSecond.next());
            }
        }
    }
}
